The purpose of a program checking tool is to analyze a given computer program to determine whether or not it has certain desirable properties. Program checking tools, often called program checkers, are specific examples of verification systems that can also be used to analyze hardware components, formulae, algorithms, or, more generally, stylistic qualities or behavioral designs. A program checking tool receives a program as input, and then outputs warning messages about the execution behavior of the program. A warning may be considered to be either spurious or valid (i.e., identifying an actual program error). A spurious warning may warn about something that is not a real error, as may arise when the theorem prover does not have enough information to generate a proof. A valid warning generally warns of a real error.
Examples of program checking tools include static checkers and dynamic checkers. Static checkers catch errors at compile time without executing the program, and are valuable because they can be applied throughout the development cycle. An example of a static checker is a type checker, which compares the types (e.g., “integer,” “floating point,” “character,” “pointer,” etc.) of functions and variables of a program. A type checker detects errors such as passing inappropriate arguments for a function call, or performing an operation of one type on a variable of another type.
Another example of a static checker is the Extended Static Checker for Java (“ESC/Java”) from Compaq Computer Corporation (Houston, Tex.), which checks for additional errors that are not caught by traditional type systems, such as dereferencing a null pointer, indexing an array outside its bounds, or accessing a shared variable without holding its protecting lock. In ESC/Java, a programmer writes an ordinary Java program but adds annotations, such as pre- and post-conditions on methods. Each annotated method is translated into a logical formula that is valid if and only if the method meets its specification. A theorem prover searches for counter-examples to the logical formula, which correspond to possible errors in the original Java method. A key design principle of ESC/Java is modular checking, which means that each method is checked in isolation, given only the specifications, and not the implementations, of other methods in the program.
In contrast to static checkers, dynamic checkers monitor for actual run-time errors. Dynamic checkers are a class of authoring tools that perform program checking functions and generate execution traces by executing or simulating the execution of the computer program in question. An example of a dynamic checker is Purify from Rational Software Corporation (Cupertino, Calif.), which instruments a binary program by adding protection instructions around every load and store operation. The instrumented instructions perform various checks at run-time, including checking for array access violations, uninitialized memory reads, and memory leaks. When the program is executed, a user interface displays the errors and warnings as they occur.
Using a program checking tool has several costs, one of which is the time required to inspect the checker's warnings to determine which are spurious and which are valid. A good program checking tool has the property that the warnings it produces are informative and easy for a programmer to understand. An informative warning message should, ideally, include a characterization of each possible defect (e.g., “array index out of bounds,” “timing constraint not satisfied,” “race condition,” “deadlock,” “failure to establish invariant,” etc.), and a source location in the computer program where the verification system tried, but failed, to show the absence of a defect (e.g., “line 218 of file ‘ABC.source’”). If a warning message is informative and easy to understand, a programmer can more easily determine whether a warning is real or spurious, as well as the nature of its cause. The programmer can then act accordingly, correcting the program at the source of the error, ignoring the warning, or annotating the program so that the warning will be suppressed next time the program checking tool is run.
However, even if a program checking tool provides informative and easy to understand warning messages, a programmer may still need to look through hundreds or thousands of warning messages, a majority of which are typically spurious. To try to reduce this burden, some program checking tools suppress all warning messages of a given kind, both spurious and valid. However, this inevitably eliminates some valid warnings. Another technique to reduce spurious warning messages is to improve the analysis of the program checking tool. However, this requires significantly more computational resources, and may still result in spurious warnings, or missed valid warnings. Yet another technique to reduce spurious warning messages is to estimate, in conjunction with the warning, the likelihood that the warning identifies an actual error, and then allow the user to filter and sort warnings based on this estimate. Again, however, this requires higher computational resources, and is only as good as the predictive heuristics of the estimator.
Therefore, it would be desirable to provide a method and apparatus of improving the warning messages generated by a program checking tool so as to allow a user to effectively and rapidly review the warning messages.